Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar16/RubioSLASHwst99.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.

↳ QTRS

  ↳ Non-Overlap Check

Q restricted rewrite system:
The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.

The TRS is non-overlapping. Hence, we can switch to innermost.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

U41₂(dout₁(DX), X) -> U42₃(din₁(der₁(DX)), X, DX)
U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(plus₂(X, Y))) -> U21₃(din₁(der₁(X)), X, Y)
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
U31₃(dout₁(DX), X, Y) -> U32₄(din₁(der₁(Y)), X, Y, DX)
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U21₃(dout₁(DX), X, Y) -> U22₄(din₁(der₁(Y)), X, Y, DX)
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U41₂(dout₁(DX), X) -> U42₃(din₁(der₁(DX)), X, DX)
U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(plus₂(X, Y))) -> U21₃(din₁(der₁(X)), X, Y)
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
U31₃(dout₁(DX), X, Y) -> U32₄(din₁(der₁(Y)), X, Y, DX)
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U21₃(dout₁(DX), X, Y) -> U22₄(din₁(der₁(Y)), X, Y, DX)
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 3 less nodes.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(plus₂(X, Y))) -> U21₃(din₁(der₁(X)), X, Y)
U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

DIN₁(der₁(plus₂(X, Y))) -> U21₃(din₁(der₁(X)), X, Y)
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)

The remaining pairs can at least by weakly be oriented.

U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

Used ordering: Combined order from the following AFS and order.
DIN₁(x1) = DIN
der₁(x1) = der₁(x1)
plus₂(x1, x2) = x1
U21₃(x1, x2, x3) = x1
din₁(x1) = din
dout₁(x1) = dout
times₂(x1, x2) = times₂(x1, x2)
U31₃(x1, x2, x3) = x1
U41₂(x1, x2) = U41
u21₃(x1, x2, x3) = u21
u31₃(x1, x2, x3) = x1
u41₂(x1, x2) = x1
u42₃(x1, x2, x3) = u42₁(x1)
u32₄(x1, x2, x3, x4) = u32₁(x1)
u22₄(x1, x2, x3, x4) = x1

Lexicographic Path Order [19].
Precedence:

der₁ > [DIN, dout, U41] > [din, u21] > [u42₁, u32_1]
times₂ > [DIN, dout, U41] > [din, u21] > [u42₁, u32_1]

The following usable rules [14] were oriented:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 2 less nodes.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The remaining pairs can at least by weakly be oriented.

DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))

Used ordering: Combined order from the following AFS and order.
DIN₁(x1) = DIN
der₁(x1) = x1
times₂(x1, x2) = times₁(x2)
plus₂(x1, x2) = plus
U41₂(x1, x2) = U41₁(x1)
dout₁(x1) = dout
din₁(x1) = din
u21₃(x1, x2, x3) = u21
u31₃(x1, x2, x3) = x1
u41₂(x1, x2) = u41
u42₃(x1, x2, x3) = x1
u32₄(x1, x2, x3, x4) = u32
u22₄(x1, x2, x3, x4) = x1

Lexicographic Path Order [19].
Precedence:

plus > [DIN, dout, u32] > times₁
plus > [DIN, dout, u32] > U41₁
plus > [DIN, dout, u32] > [din, u21, u41]

The following usable rules [14] were oriented:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))

The remaining pairs can at least by weakly be oriented.

DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))

Used ordering: Combined order from the following AFS and order.
DIN₁(x1) = x1
der₁(x1) = der₁(x1)
times₂(x1, x2) = x1
plus₂(x1, x2) = x1

Lexicographic Path Order [19].
Precedence:

trivial

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))

The remaining pairs can at least by weakly be oriented.

DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))

Used ordering: Combined order from the following AFS and order.
DIN₁(x1) = DIN₁(x1)
der₁(x1) = x1
times₂(x1, x2) = x1
plus₂(x1, x2) = plus₁(x1)

Lexicographic Path Order [19].
Precedence:

plus₁ > DIN₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

                                ↳ QDP

                                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
DIN₁(x1) = DIN₁(x1)
der₁(x1) = der₁(x1)
times₂(x1, x2) = times₁(x1)

Lexicographic Path Order [19].
Precedence:

[DIN₁, der_1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

                                      ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

The set Q consists of the following terms:

din₁(der₁(plus₂(x0, x1)))
u21₃(dout₁(x0), x1, x2)
u22₄(dout₁(x0), x1, x2, x3)
din₁(der₁(times₂(x0, x1)))
u31₃(dout₁(x0), x1, x2)
u32₄(dout₁(x0), x1, x2, x3)
din₁(der₁(der₁(x0)))
u41₂(dout₁(x0), x1)
u42₃(dout₁(x0), x1, x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.